$\forall$$T$:Type, ${\it as}_{2}$, ${\it bs}_{2}$, ${\it as}_{1}$, ${\it bs}_{1}$:$T$ List.
\\[0ex]${\it as}_{1}$ $\leq$ ${\it as}_{2}$ $\Rightarrow$ ${\it bs}_{1}$ $\leq$ ${\it bs}_{2}$ $\Rightarrow$ agree\_on\_common($T$;${\it as}_{2}$;${\it bs}_{2}$) $\Rightarrow$ agree\_on\_common($T$;${\it as}_{1}$;${\it bs}_{1}$)